#!/bin/sh
pdflatex manual
makeindex manual
pdflatex manual
#cp manual.pdf ../  # should copy manually to avoid checking in every minor change to the manual
